$\forall$$A$:Type\{i\}, $e$:$A$, $H$:($A$$\rightarrow$Type\{j\}), $z$:$H$($e$). $z$ $\neq$ 0 $\in$ $\mathbb{Z}$